The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).

0 CpxTRS
    ↳1 CpxTrsMatchBoundsTAProof (⇔, 305 ms)
    ↳2 BOUNDS(1, n^1)
    ↳3 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳4 CdtProblem
        ↳5 CdtLeafRemovalProof (ComplexityIfPolyImplication, 0 ms)
        ↳6 CdtProblem
        ↳7 CdtUsableRulesProof (⇔, 0 ms)
        ↳8 CdtProblem
        ↳9 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 86 ms)
        ↳10 CdtProblem
        ↳11 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 13 ms)
        ↳12 CdtProblem
        ↳13 SIsEmptyProof (BOTH BOUNDS(ID, ID), 0 ms)
        ↳14 BOUNDS(1, 1)

(0) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

revconsapp(C(x1, x2), r) → revconsapp(x2, C(x1, r))
deeprevapp(C(x1, x2), rest) → deeprevapp(x2, C(x1, rest))
deeprevapp(V(n), rest) → revconsapp(rest, V(n))
deeprevapp(N, rest) → rest
revconsapp(V(n), r) → r
revconsapp(N, r) → r
deeprev(C(x1, x2)) → deeprevapp(C(x1, x2), N)
deeprev(V(n)) → V(n)
deeprev(N) → N
second(V(n)) → N
second(C(x1, x2)) → x2
isVal(C(x1, x2)) → False
isVal(V(n)) → True
isVal(N) → False
isNotEmptyT(C(x1, x2)) → True
isNotEmptyT(V(n)) → False
isNotEmptyT(N) → False
isEmptyT(C(x1, x2)) → False
isEmptyT(V(n)) → False
isEmptyT(N) → True
first(V(n)) → N
first(C(x1, x2)) → x1
goal(x) → deeprev(x)

Rewrite Strategy: INNERMOST

(1) CpxTrsMatchBoundsTAProof (EQUIVALENT transformation)

A linear upper bound on the runtime complexity of the TRS R could be shown with a Match-Bound[TAB_LEFTLINEAR,TAB_NONLEFTLINEAR] (for contructor-based start-terms) of 3.

The compatible tree automaton used to show the Match-Boundedness (for constructor-based start-terms) is represented by:
final states : [1, 2, 3, 4, 5, 6, 7, 8, 9]
transitions:
C0(0, 0) → 0
V0(0) → 0
N0() → 0
False0() → 0
True0() → 0
revconsapp0(0, 0) → 1
deeprevapp0(0, 0) → 2
deeprev0(0) → 3
second0(0) → 4
isVal0(0) → 5
isNotEmptyT0(0) → 6
isEmptyT0(0) → 7
first0(0) → 8
goal0(0) → 9
C1(0, 0) → 10
revconsapp1(0, 10) → 1
C1(0, 0) → 11
deeprevapp1(0, 11) → 2
V1(0) → 12
revconsapp1(0, 12) → 2
C1(0, 0) → 13
N1() → 14
deeprevapp1(13, 14) → 3
V1(0) → 3
N1() → 3
N1() → 4
False1() → 5
True1() → 5
True1() → 6
False1() → 6
False1() → 7
True1() → 7
N1() → 8
deeprev1(0) → 9
C1(0, 10) → 10
C1(0, 12) → 10
revconsapp1(0, 10) → 2
C1(0, 11) → 11
C2(0, 14) → 15
deeprevapp2(0, 15) → 3
revconsapp1(11, 12) → 2
deeprevapp1(13, 14) → 9
V1(0) → 9
N1() → 9
C2(0, 12) → 16
revconsapp2(0, 16) → 2
revconsapp2(11, 16) → 2
deeprevapp2(0, 15) → 9
C1(0, 15) → 11
deeprevapp1(0, 11) → 3
revconsapp1(15, 12) → 3
revconsapp2(15, 16) → 2
revconsapp1(11, 12) → 3
revconsapp2(14, 16) → 3
deeprevapp1(0, 11) → 9
revconsapp1(15, 12) → 9
C1(0, 16) → 10
C2(0, 16) → 16
revconsapp2(0, 16) → 3
revconsapp2(11, 16) → 3
revconsapp2(15, 16) → 3
revconsapp1(11, 12) → 9
revconsapp2(14, 16) → 9
C3(0, 16) → 17
revconsapp3(14, 17) → 2
revconsapp2(0, 16) → 9
revconsapp2(11, 16) → 9
revconsapp2(15, 16) → 9
revconsapp1(0, 10) → 3
revconsapp3(14, 17) → 3
revconsapp1(0, 10) → 9
revconsapp3(14, 17) → 9
0 → 2
0 → 1
0 → 4
0 → 8
11 → 2
11 → 3
11 → 9
10 → 1
10 → 2
10 → 3
10 → 9
12 → 2
15 → 3
15 → 9
16 → 2
16 → 3
16 → 9
17 → 2
17 → 3
17 → 9

(2) BOUNDS(1, n^1)

(3) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted Cpx (relative) TRS to CDT

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

revconsapp(C(z0, z1), z2) → revconsapp(z1, C(z0, z2))
revconsapp(V(z0), z1) → z1
revconsapp(N, z0) → z0
deeprevapp(C(z0, z1), z2) → deeprevapp(z1, C(z0, z2))
deeprevapp(V(z0), z1) → revconsapp(z1, V(z0))
deeprevapp(N, z0) → z0
deeprev(C(z0, z1)) → deeprevapp(C(z0, z1), N)
deeprev(V(z0)) → V(z0)
deeprev(N) → N
second(V(z0)) → N
second(C(z0, z1)) → z1
isVal(C(z0, z1)) → False
isVal(V(z0)) → True
isVal(N) → False
isNotEmptyT(C(z0, z1)) → True
isNotEmptyT(V(z0)) → False
isNotEmptyT(N) → False
isEmptyT(C(z0, z1)) → False
isEmptyT(V(z0)) → False
isEmptyT(N) → True
first(V(z0)) → N
first(C(z0, z1)) → z0
goal(z0) → deeprev(z0)
Tuples:

REVCONSAPP(C(z0, z1), z2) → c(REVCONSAPP(z1, C(z0, z2)))
REVCONSAPP(V(z0), z1) → c1
REVCONSAPP(N, z0) → c2
DEEPREVAPP(C(z0, z1), z2) → c3(DEEPREVAPP(z1, C(z0, z2)))
DEEPREVAPP(V(z0), z1) → c4(REVCONSAPP(z1, V(z0)))
DEEPREVAPP(N, z0) → c5
DEEPREV(C(z0, z1)) → c6(DEEPREVAPP(C(z0, z1), N))
DEEPREV(V(z0)) → c7
DEEPREV(N) → c8
SECOND(V(z0)) → c9
SECOND(C(z0, z1)) → c10
ISVAL(C(z0, z1)) → c11
ISVAL(V(z0)) → c12
ISVAL(N) → c13
ISNOTEMPTYT(C(z0, z1)) → c14
ISNOTEMPTYT(V(z0)) → c15
ISNOTEMPTYT(N) → c16
ISEMPTYT(C(z0, z1)) → c17
ISEMPTYT(V(z0)) → c18
ISEMPTYT(N) → c19
FIRST(V(z0)) → c20
FIRST(C(z0, z1)) → c21
GOAL(z0) → c22(DEEPREV(z0))
S tuples:

REVCONSAPP(C(z0, z1), z2) → c(REVCONSAPP(z1, C(z0, z2)))
REVCONSAPP(V(z0), z1) → c1
REVCONSAPP(N, z0) → c2
DEEPREVAPP(C(z0, z1), z2) → c3(DEEPREVAPP(z1, C(z0, z2)))
DEEPREVAPP(V(z0), z1) → c4(REVCONSAPP(z1, V(z0)))
DEEPREVAPP(N, z0) → c5
DEEPREV(C(z0, z1)) → c6(DEEPREVAPP(C(z0, z1), N))
DEEPREV(V(z0)) → c7
DEEPREV(N) → c8
SECOND(V(z0)) → c9
SECOND(C(z0, z1)) → c10
ISVAL(C(z0, z1)) → c11
ISVAL(V(z0)) → c12
ISVAL(N) → c13
ISNOTEMPTYT(C(z0, z1)) → c14
ISNOTEMPTYT(V(z0)) → c15
ISNOTEMPTYT(N) → c16
ISEMPTYT(C(z0, z1)) → c17
ISEMPTYT(V(z0)) → c18
ISEMPTYT(N) → c19
FIRST(V(z0)) → c20
FIRST(C(z0, z1)) → c21
GOAL(z0) → c22(DEEPREV(z0))
K tuples:none
Defined Rule Symbols:

revconsapp, deeprevapp, deeprev, second, isVal, isNotEmptyT, isEmptyT, first, goal

Defined Pair Symbols:

REVCONSAPP, DEEPREVAPP, DEEPREV, SECOND, ISVAL, ISNOTEMPTYT, ISEMPTYT, FIRST, GOAL

Compound Symbols:

c, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20, c21, c22

(5) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 2 leading nodes:

GOAL(z0) → c22(DEEPREV(z0))
DEEPREV(C(z0, z1)) → c6(DEEPREVAPP(C(z0, z1), N))
Removed 18 trailing nodes:

DEEPREVAPP(N, z0) → c5
REVCONSAPP(N, z0) → c2
REVCONSAPP(V(z0), z1) → c1
ISEMPTYT(C(z0, z1)) → c17
SECOND(V(z0)) → c9
SECOND(C(z0, z1)) → c10
FIRST(C(z0, z1)) → c21
ISEMPTYT(N) → c19
ISNOTEMPTYT(C(z0, z1)) → c14
ISEMPTYT(V(z0)) → c18
ISVAL(N) → c13
ISNOTEMPTYT(V(z0)) → c15
ISNOTEMPTYT(N) → c16
DEEPREV(N) → c8
FIRST(V(z0)) → c20
DEEPREV(V(z0)) → c7
ISVAL(V(z0)) → c12
ISVAL(C(z0, z1)) → c11

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

revconsapp(C(z0, z1), z2) → revconsapp(z1, C(z0, z2))
revconsapp(V(z0), z1) → z1
revconsapp(N, z0) → z0
deeprevapp(C(z0, z1), z2) → deeprevapp(z1, C(z0, z2))
deeprevapp(V(z0), z1) → revconsapp(z1, V(z0))
deeprevapp(N, z0) → z0
deeprev(C(z0, z1)) → deeprevapp(C(z0, z1), N)
deeprev(V(z0)) → V(z0)
deeprev(N) → N
second(V(z0)) → N
second(C(z0, z1)) → z1
isVal(C(z0, z1)) → False
isVal(V(z0)) → True
isVal(N) → False
isNotEmptyT(C(z0, z1)) → True
isNotEmptyT(V(z0)) → False
isNotEmptyT(N) → False
isEmptyT(C(z0, z1)) → False
isEmptyT(V(z0)) → False
isEmptyT(N) → True
first(V(z0)) → N
first(C(z0, z1)) → z0
goal(z0) → deeprev(z0)
Tuples:

REVCONSAPP(C(z0, z1), z2) → c(REVCONSAPP(z1, C(z0, z2)))
DEEPREVAPP(C(z0, z1), z2) → c3(DEEPREVAPP(z1, C(z0, z2)))
DEEPREVAPP(V(z0), z1) → c4(REVCONSAPP(z1, V(z0)))
S tuples:

REVCONSAPP(C(z0, z1), z2) → c(REVCONSAPP(z1, C(z0, z2)))
DEEPREVAPP(C(z0, z1), z2) → c3(DEEPREVAPP(z1, C(z0, z2)))
DEEPREVAPP(V(z0), z1) → c4(REVCONSAPP(z1, V(z0)))
K tuples:none
Defined Rule Symbols:

revconsapp, deeprevapp, deeprev, second, isVal, isNotEmptyT, isEmptyT, first, goal

Defined Pair Symbols:

REVCONSAPP, DEEPREVAPP

Compound Symbols:

c, c3, c4

(7) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

revconsapp(C(z0, z1), z2) → revconsapp(z1, C(z0, z2))
revconsapp(V(z0), z1) → z1
revconsapp(N, z0) → z0
deeprevapp(C(z0, z1), z2) → deeprevapp(z1, C(z0, z2))
deeprevapp(V(z0), z1) → revconsapp(z1, V(z0))
deeprevapp(N, z0) → z0
deeprev(C(z0, z1)) → deeprevapp(C(z0, z1), N)
deeprev(V(z0)) → V(z0)
deeprev(N) → N
second(V(z0)) → N
second(C(z0, z1)) → z1
isVal(C(z0, z1)) → False
isVal(V(z0)) → True
isVal(N) → False
isNotEmptyT(C(z0, z1)) → True
isNotEmptyT(V(z0)) → False
isNotEmptyT(N) → False
isEmptyT(C(z0, z1)) → False
isEmptyT(V(z0)) → False
isEmptyT(N) → True
first(V(z0)) → N
first(C(z0, z1)) → z0
goal(z0) → deeprev(z0)

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:none
Tuples:

REVCONSAPP(C(z0, z1), z2) → c(REVCONSAPP(z1, C(z0, z2)))
DEEPREVAPP(C(z0, z1), z2) → c3(DEEPREVAPP(z1, C(z0, z2)))
DEEPREVAPP(V(z0), z1) → c4(REVCONSAPP(z1, V(z0)))
S tuples:

REVCONSAPP(C(z0, z1), z2) → c(REVCONSAPP(z1, C(z0, z2)))
DEEPREVAPP(C(z0, z1), z2) → c3(DEEPREVAPP(z1, C(z0, z2)))
DEEPREVAPP(V(z0), z1) → c4(REVCONSAPP(z1, V(z0)))
K tuples:none
Defined Rule Symbols:none

Defined Pair Symbols:

REVCONSAPP, DEEPREVAPP

Compound Symbols:

c, c3, c4

(9) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

DEEPREVAPP(V(z0), z1) → c4(REVCONSAPP(z1, V(z0)))
We considered the (Usable) Rules:none
And the Tuples:

REVCONSAPP(C(z0, z1), z2) → c(REVCONSAPP(z1, C(z0, z2)))
DEEPREVAPP(C(z0, z1), z2) → c3(DEEPREVAPP(z1, C(z0, z2)))
DEEPREVAPP(V(z0), z1) → c4(REVCONSAPP(z1, V(z0)))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(C(x1, x2)) = x2   
POL(DEEPREVAPP(x1, x2)) = [1] + x1 + x2   
POL(REVCONSAPP(x1, x2)) = 0   
POL(V(x1)) = [1]   
POL(c(x1)) = x1   
POL(c3(x1)) = x1   
POL(c4(x1)) = x1   

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:none
Tuples:

REVCONSAPP(C(z0, z1), z2) → c(REVCONSAPP(z1, C(z0, z2)))
DEEPREVAPP(C(z0, z1), z2) → c3(DEEPREVAPP(z1, C(z0, z2)))
DEEPREVAPP(V(z0), z1) → c4(REVCONSAPP(z1, V(z0)))
S tuples:

REVCONSAPP(C(z0, z1), z2) → c(REVCONSAPP(z1, C(z0, z2)))
DEEPREVAPP(C(z0, z1), z2) → c3(DEEPREVAPP(z1, C(z0, z2)))
K tuples:

DEEPREVAPP(V(z0), z1) → c4(REVCONSAPP(z1, V(z0)))
Defined Rule Symbols:none

Defined Pair Symbols:

REVCONSAPP, DEEPREVAPP

Compound Symbols:

c, c3, c4

(11) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

REVCONSAPP(C(z0, z1), z2) → c(REVCONSAPP(z1, C(z0, z2)))
DEEPREVAPP(C(z0, z1), z2) → c3(DEEPREVAPP(z1, C(z0, z2)))
We considered the (Usable) Rules:none
And the Tuples:

REVCONSAPP(C(z0, z1), z2) → c(REVCONSAPP(z1, C(z0, z2)))
DEEPREVAPP(C(z0, z1), z2) → c3(DEEPREVAPP(z1, C(z0, z2)))
DEEPREVAPP(V(z0), z1) → c4(REVCONSAPP(z1, V(z0)))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(C(x1, x2)) = [2] + x2   
POL(DEEPREVAPP(x1, x2)) = [2] + [3]x1 + [2]x2   
POL(REVCONSAPP(x1, x2)) = [1] + [2]x1   
POL(V(x1)) = [2] + x1   
POL(c(x1)) = x1   
POL(c3(x1)) = x1   
POL(c4(x1)) = x1   

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:none
Tuples:

REVCONSAPP(C(z0, z1), z2) → c(REVCONSAPP(z1, C(z0, z2)))
DEEPREVAPP(C(z0, z1), z2) → c3(DEEPREVAPP(z1, C(z0, z2)))
DEEPREVAPP(V(z0), z1) → c4(REVCONSAPP(z1, V(z0)))
S tuples:none
K tuples:

DEEPREVAPP(V(z0), z1) → c4(REVCONSAPP(z1, V(z0)))
REVCONSAPP(C(z0, z1), z2) → c(REVCONSAPP(z1, C(z0, z2)))
DEEPREVAPP(C(z0, z1), z2) → c3(DEEPREVAPP(z1, C(z0, z2)))
Defined Rule Symbols:none

Defined Pair Symbols:

REVCONSAPP, DEEPREVAPP

Compound Symbols:

c, c3, c4

(13) SIsEmptyProof (BOTH BOUNDS(ID, ID) transformation)

The set S is empty

(14) BOUNDS(1, 1)